R. G. Jeroslow; "Redundancies in the Hilbert–Bernays Derivability Conditions for Gödel's Second Incompleteness Theorem"
https://scrapbox.io/files/6502137094f01f001be7d445.pdf
著者
R. G. Jeroslow
Def: Jeroslow文
Thm: Jeroslowの第2不完全性定理
$ \bf D1と形式化されたΣ₁完全性定理$ \bf \Sigma_1Cを満たす証明可能性述語$ \mathbf{Pr}_T(x)について，
$ T \nvdash \forall_x.\lbrack \mathrm{Fml}(x) \land \mathrm{Pr}_T(x) \to \lnot\mathrm{Pr}_T(\dot{\lnot} x) \rbrack
remark:
$ \dot\lnot x = \ulcorner \lnot E_x \urcorner．